(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(n__a, X, X) → f(activate(X), b, n__b)
b → a
a → n__a
b → n__b
activate(n__a) → a
activate(n__b) → b
activate(X) → X
Q is empty.
(1) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, X, X) → F(activate(X), b, n__b)
F(n__a, X, X) → ACTIVATE(X)
F(n__a, X, X) → B
B → A
ACTIVATE(n__a) → A
ACTIVATE(n__b) → B
The TRS R consists of the following rules:
f(n__a, X, X) → f(activate(X), b, n__b)
b → a
a → n__a
b → n__b
activate(n__a) → a
activate(n__b) → b
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 5 less nodes.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, X, X) → F(activate(X), b, n__b)
The TRS R consists of the following rules:
f(n__a, X, X) → f(activate(X), b, n__b)
b → a
a → n__a
b → n__b
activate(n__a) → a
activate(n__b) → b
activate(X) → X
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(5) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, X, X) → F(activate(X), b, n__b)
The TRS R consists of the following rules:
activate(n__a) → a
activate(n__b) → b
activate(X) → X
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(7) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
F(
n__a,
X,
X) →
F(
activate(
X),
b,
n__b) at position [0] we obtained the following new rules [LPAR04]:
F(n__a, n__a, n__a) → F(a, b, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)
F(n__a, x0, x0) → F(x0, b, n__b)
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__a, n__a) → F(a, b, n__b)
F(n__a, n__b, n__b) → F(b, b, n__b)
F(n__a, x0, x0) → F(x0, b, n__b)
The TRS R consists of the following rules:
activate(n__a) → a
activate(n__b) → b
activate(X) → X
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(9) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(10) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(b, b, n__b)
F(n__a, x0, x0) → F(x0, b, n__b)
The TRS R consists of the following rules:
activate(n__a) → a
activate(n__b) → b
activate(X) → X
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(11) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(b, b, n__b)
F(n__a, x0, x0) → F(x0, b, n__b)
The TRS R consists of the following rules:
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(13) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
F(
n__a,
n__b,
n__b) →
F(
b,
b,
n__b) at position [0] we obtained the following new rules [LPAR04]:
F(n__a, n__b, n__b) → F(a, b, n__b)
F(n__a, n__b, n__b) → F(n__b, b, n__b)
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, x0, x0) → F(x0, b, n__b)
F(n__a, n__b, n__b) → F(a, b, n__b)
F(n__a, n__b, n__b) → F(n__b, b, n__b)
The TRS R consists of the following rules:
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(15) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, x0, x0) → F(x0, b, n__b)
F(n__a, n__b, n__b) → F(a, b, n__b)
The TRS R consists of the following rules:
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(17) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
F(
n__a,
x0,
x0) →
F(
x0,
b,
n__b) at position [] we obtained the following new rules [LPAR04]:
F(n__a, y0, y0) → F(y0, a, n__b)
F(n__a, y0, y0) → F(y0, n__b, n__b)
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(a, b, n__b)
F(n__a, y0, y0) → F(y0, a, n__b)
F(n__a, y0, y0) → F(y0, n__b, n__b)
The TRS R consists of the following rules:
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(19) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
F(
n__a,
n__b,
n__b) →
F(
a,
b,
n__b) at position [0] we obtained the following new rules [LPAR04]:
F(n__a, n__b, n__b) → F(n__a, b, n__b)
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, y0, y0) → F(y0, a, n__b)
F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, b, n__b)
The TRS R consists of the following rules:
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(21) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
F(
n__a,
y0,
y0) →
F(
y0,
a,
n__b) at position [] we obtained the following new rules [LPAR04]:
F(n__a, y0, y0) → F(y0, n__a, n__b)
(22) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, b, n__b)
F(n__a, y0, y0) → F(y0, n__a, n__b)
The TRS R consists of the following rules:
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(23) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(24) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, b, n__b)
The TRS R consists of the following rules:
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(25) Narrowing (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
F(
n__a,
n__b,
n__b) →
F(
n__a,
b,
n__b) at position [] we obtained the following new rules [LPAR04]:
F(n__a, n__b, n__b) → F(n__a, a, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
(26) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, a, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
The TRS R consists of the following rules:
b → a
b → n__b
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(27) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(28) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, a, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
The TRS R consists of the following rules:
a → n__a
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(29) MNOCProof (EQUIVALENT transformation)
We use the modular non-overlap check [LPAR04] to enlarge Q to all left-hand sides of R.
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, a, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
The TRS R consists of the following rules:
a → n__a
The set Q consists of the following terms:
a
We have to consider all minimal (P,Q,R)-chains.
(31) Rewriting (EQUIVALENT transformation)
By rewriting [LPAR04] the rule
F(
n__a,
n__b,
n__b) →
F(
n__a,
a,
n__b) at position [1] we obtained the following new rules [LPAR04]:
F(n__a, n__b, n__b) → F(n__a, n__a, n__b)
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, n__a, n__b)
The TRS R consists of the following rules:
a → n__a
The set Q consists of the following terms:
a
We have to consider all minimal (P,Q,R)-chains.
(33) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
The TRS R consists of the following rules:
a → n__a
The set Q consists of the following terms:
a
We have to consider all minimal (P,Q,R)-chains.
(35) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(36) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
R is empty.
The set Q consists of the following terms:
a
We have to consider all minimal (P,Q,R)-chains.
(37) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
a
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, y0, y0) → F(y0, n__b, n__b)
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(39) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
F(
n__a,
y0,
y0) →
F(
y0,
n__b,
n__b) we obtained the following new rules [LPAR04]:
F(n__a, n__b, n__b) → F(n__b, n__b, n__b)
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
F(n__a, n__b, n__b) → F(n__b, n__b, n__b)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(41) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(n__a, n__b, n__b) → F(n__a, n__b, n__b)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(43) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.
s =
F(
n__a,
n__b,
n__b) evaluates to t =
F(
n__a,
n__b,
n__b)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequenceThe DP semiunifies directly so there is only one rewrite step from F(n__a, n__b, n__b) to F(n__a, n__b, n__b).
(44) NO